$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$). $P$ $\Rightarrow$ $P$